Jane Street builds its trading systems in OCaml, relying on the type system to catch errors at compile time and avoid run-time crashes. They snapshot every successful build to train an in-house AI model, rewarding only code changes that compile and pass tests.

• Jane Street runs its trading systems almost entirely on OCaml, betting on compile-time type checking (e.g., mandatory Option handling) to prevent costly runtime bugs.
• They rejected off-the-shelf tools like Copilot and Claude in favor of an in-house AI model trained on their own workspace snapshots.
• Developer workspaces are snapshotted every 20 seconds, and reinforcement learning rewards only edits that compile and pass tests.
• This snapshot-trained system underpins infrastructure supporting roughly $40 billion in annual trading volume.

Jane Street had long skipped full-on formal methods despite using advanced type systems, but the rise of agent-driven coding cut proof costs and widened access. They’re now forming a team to integrate formal verification into their OCaml toolchain, tweaking the language and tapping their experienced user base while collaborating with external proof ecosystems.

• seL4's formal verification cost 25 person-years for 8,700 lines of C (23 lines of proof per code line, half a person-day per line), illustrating why Jane Street long saw full formal methods as impractical.
• Agentic AI coding flips that math: it lowers the cost of generating proofs and widens access to formal methods, but also produces messy code that creates a new "verification bottleneck."
• Jane Street is building an internal formal-methods team to extend OCaml itself (modular specs, ownership/mutability typing, embedded tactics) rather than switch to tools like Lean, Dafny, or Coq, while still integrating those ecosystems where useful.
• The plan is to use formal verification both to catch bugs in AI-generated code and to feed precise feedback back into training/improving the coding agents.